// port of Freshlib 0.1 (http://homepages.inf.ed.ac.uk/jcheney/FreshLib.html/FreshLib-0.1-src.tar.gz) to Scala
// Author: Adriaan Moors (19 July 2007)

/*package scala.examples.tcpoly.binding.frescala.idiomatic

import scala.examples.tcpoly.idioms._
import scala.examples.tcpoly.monads._

// abstraction monad
trait AbsM extends MonadIdioms {
  type Tag = Int
  def Tag(i: Int): Tag = i
  
  object AM {
    def apply[a](fun: Int => (a, Int)) = new AM(fun)
    def newTag = AM{i => (Tag(i), i+1)}
  }
  
  class AM[+a](val fun: Int => (a, Int)) {
    def run = fun(0)._1
  }

  implicit object AMisMonad extends Monad[AM] {
    def >>=[A, B](f: A => AM[B])(implicit self: AM[A]): AM[B] = AM( (i: Int) => 
        (self.fun(i) match { case (a, next) => f(a).fun(next) }))
    def result[A](x: A) = AM((x, _))
  }
  //import AMisMonad.{witness, result} // the imported members seem not to be inherited!
  implicit def AMwitness[B](x: AM[B]) = AMisMonad.witness(x)
  implicit def AMresult[A](x: A) = AMisMonad.result(x)

  implicit object AMisIdiom extends MonadicIdiom[AM]
}

trait Binding extends Idioms with MonoidIdioms  { self: BindingSyntax with Binding => 
  trait Nominal[Self] {
    val injectNominal: IFunctor[Self, Nominal]
    import injectNominal._
    
    def swap(a: Name, b: Name): Self = inject[Id](new PolyFun1[Id, Id, Nominal, Self] { def apply[T >: Self](x: T)(implicit c: T => Nominal[T]) =
       x.swap(a, b) })
    def fresh(a: Name): Boolean = inject[Const1[Boolean]#Apply](new PolyFun1[Id, Const1[Boolean]#Apply, Nominal, Self] { def apply[T >: Self](x: T)(implicit c: T => Nominal[T]) =
      x.fresh(a) })
    def supp: List[Name] = inject[Const1[List[Name]]#Apply](new PolyFun1[Id, Const1[List[Name]]#Apply, Nominal, Self] { def apply[T >: Self](x: T)(implicit c: T => Nominal[T]) =
      x.supp })
  }

  implicit def IntIsNominal(self: Int): Nominal[Int] = new Nominal[Int] {
    object injectNominal extends IFunctor[Int, Nominal] {
      def inject[I[+_]](f: InjFun[I])(implicit idi: Idiom[I]) = idi.^^(self)
    }
      
/*  def swap(a: Name, b: Name) = self
    def fresh(a: Name) = true
    def supp = List()*/
  }  

  implicit def CharIsNominal(self: Char): Nominal[Char] = new Nominal[Char] {
    object injectNominal extends IFunctor[Char, Nominal] {
      def inject[I[+_]](f: InjFun[I])(implicit idi: Idiom[I]) = idi.^^(self)
    }
    
/*  def swap(a: Name, b: Name) = self
    def fresh(a: Name) = true
    def supp = List()*/
  } 
  
  implicit def UnitIsNominal(self: Unit): Nominal[Unit] = new Nominal[Unit] {
    object injectNominal extends IFunctor[Unit, Nominal] {
      def inject[I[+_]](f: InjFun[I])(implicit idi: Idiom[I]) = idi.^^(self)
    }      
    
/*  def swap(a: Name, b: Name) = self
    def fresh(a: Name) = true
    def supp = List()*/
  }   
  
  implicit def IterableIsNominal[T <% Nominal[T]](self: Iterable[T]): Nominal[Iterable[T]] = new Nominal[Iterable[T]] {
    object injectNominal extends IFunctor[Iterable[T], Nominal] {    
      def inject[I[+_]](f: InjFun[I])(implicit idi: Idiom[I]) = error("TODO") // TODO: would be sensible to implement this
    }
    
    override def swap(a: Name, b: Name) = self map (_.swap(a, b))    
    override def fresh(a: Name) = self forall (_.fresh(a))
    override def supp = (self flatMap (_.supp)).toList
  }   
}

trait Substitution { self: AbsM  with Binding with BindingSyntax with Substitution =>
  trait Substable[SubstRes, +Self] { 
    type SubstableTo[+t] = Substable[SubstRes, t]
    val injectSubstable: IFunctor[Self, SubstableTo]
    import injectSubstable._
    
    def subst(sub: Name => Option[SubstRes]): AM[Self] = inject[AM](new PolyFun1[Id, AM, SubstableTo, Self] { def apply[T >: Self](x: T)(implicit c: T => SubstableTo[T]) =
       x.subst(sub) })
  }
}

trait BindingSyntax { self: AbsM with Binding with Substitution with BindingSyntax =>
  case class Name(tag: Tag, s: String) extends Nominal[Name] {
    def \\[T <: Substable[T, T]](body: T)(implicit c: T => Nominal[T]): \\[T] = new \\[T](this, body)
    
    override def equals(o: Any): Boolean = o match {
      case Name(t, _) if tag == t => true
      case _ => false
    }
    
    object injectNominal extends IFunctor[Name, Nominal] { // not used
      def inject[I[+_]](f: InjFun[I])(implicit idi: Idiom[I]) = idi.^^(Name.this)
    }
    
    override def swap(a: Name, b: Name) = if(this == a) b else if(this == b) a else this
    override def fresh(a: Name) = this != a
    override def supp = List(this)    
    
    override def toString = s + "$" + tag
  }

  def gensym(s: String): AM[Name] = for( t <- AM.newTag) yield Name(t, s)
  def rename(a: Name): AM[Name] = for( t <- AM.newTag) yield Name(t, a.s)

  class \\[T <: Substable[T, T]](private[\\] val binder: Name, 
                                 private[\\] val body: T)(implicit c: T => Nominal[T]) 
      extends Substable[T, \\[T]] with Nominal[\\[T]] {
        
    def unabs: AM[(Name, T)] = for(newBinder <- rename(binder)) 
        yield (newBinder, body swap (binder, newBinder))
        
    override def equals(o: Any): Boolean = o match {
      case other: \\[T] => (binder == other.binder && body == other.body) ||  // TODO: unchecked!
          (other.body.fresh(binder) && body == other.body.swap(binder, other.binder))
      case _ => false
    }
  
    val injectSubstable = null // non-standard implementation of subst, not worth the effort defining injectSubstable -- TODO: avoid null
   /* object injectSubstable extends IFunctor[\\[T], SubstableTo] {
      def inject[I[+_]](f: InjFun[I])(implicit idi: Idiom[I]): I[\\[T]] 
        = error("")//idi.a[T, \\[T]](idi.c2(\\.apply(_: Name, _: T)(c)) >> f(self.binder)) >> f(self.body: T)(error(""))
    }  */
    override def subst(sub: Name => Option[T]): AM[\\[T]] = for(
        bibo <- unabs;             // TODO: use unapply pattern to
        val (binder, body) = bibo; // bind (binder, body) directly
        body2 <- body subst(sub))
        yield (binder \\ body2)

    val injectNominal = null // non-standard implementation of fresh, not worth the effort defining injectSubstable -- TODO: avoid null
    /*object injectNominal extends IFunctor[\\[T], Nominal] {
      def inject[I[+_]](f: InjFun[I])(implicit idi: Idiom[I]): I[\\[T]] 
        = error("")//idi.a[T, \\[T]](idi.c2(\\.apply(_: Name, _: T)(c)) >> f(self.binder)) >> f(self.body: T)(error(""))
    }*/        
    override def swap(a: Name, b: Name) = \\(binder swap(a, b), body swap(a, b)) // boilerplate
    override def fresh(a: Name) = if(a == binder) true else body fresh (a)
    override def supp = body.supp filter (_ != binder)        
    
    override def toString = (for(
        bibo <- unabs;             
        val (binder, body) = bibo)
        yield binder + "\\\\" + body).run // NOTE: only useful for local debug output
  }

  object \\ {
    def apply[T <: Substable[T, T]](binder: Name, body: T)(implicit c: T => Nominal[T]) = new \\[T](binder, body)
    def unapply[T <: Substable[T, T]](scrutinee: \\[T])(implicit c: T => Nominal[T]): Option[AM[(Name, T)]] 
      = Some(scrutinee unabs)
  }
}

/*trait AlphaEquality { self: BindingSyntax with AlphaEquality => 
  trait AlphaEquals[T] { val self: T; implicit def witness(x: T): AlphaEquals[T]
    def =@=(other: T): Boolean
    def !@=(other: T): Boolean = !(self =@= other)
  }
  
  implicit def NameAdmitsAlphaEquality(x: Name): AlphaEquals[Name] = new AlphaEquals[Name] { 
    val self = x; implicit def witness(x: Name) = NameAdmitsAlphaEquality(x) 
    def =@=(other: Name) = self.tag == other.tag
  }
    
  implicit def AbsAdmitsAlphaEquality[T <% AlphaEquals[T]](x: \\[T]): AlphaEquals[\\[T]] = new AlphaEquals[\\[T]] { 
    val self = x; implicit def witness(x: \\[T]) = AbsAdmitsAlphaEquality(x) 
    def =@=(other: \\[T]) = (self.binder =@= other.binder && self.body =@= other.body) ||
      (other.body.fresh(self.binder) && self.body =@= other.body.swap(self.binder, other.binder))
  }   

}*/


trait Lambda { self: AbsM with Binding with Substitution with BindingSyntax with Lambda =>
  sealed abstract class Term extends Substable[Term, Term] with Nominal[Term]

  case class Var(n: Name) extends Term {
    object injectNominal extends IFunctor[Term, Nominal] {
      def inject[I[+_]](f: InjFun[I])(implicit idi: Idiom[I]) = idi.c(Var) >> f.apply(n)
    }    
    
/*  def swap(a: Name, b: Name) = Var(n swap(a, b))    
    def fresh(a: Name) = n fresh(a)
    def supp = n supp*/
    
    val injectSubstable = null
    override def subst(sub: Name => Option[Term]): AM[Term] = (sub(n).getOrElse[Term](this))
  }
  
  case class App(fun: Term, arg: Term) extends Term {
    object injectNominal extends IFunctor[Term, Nominal] {
      def inject[I[+_]](f: InjFun[I])(implicit idi: Idiom[I]) = idi.a(idi.c2(App) >> f(fun)) >> f(arg)
    }
    object injectSubstable extends IFunctor[Term, SubstableTo] {
      def inject[I[+_]](f: InjFun[I])(implicit idi: Idiom[I]) = idi.a(idi.c2(App) >> f(fun)) >> f(arg)
    }      
    
/*  def swap(a: Name, b: Name) = App(fun swap(a, b), arg swap(a, b))
    def fresh(a: Name) = fun.fresh(a) && arg.fresh(a)
    def supp = fun.supp ::: arg.supp

    def subst(sub: Name => Option[Term]): AM[Term] =  for(
      f2 <- fun subst(sub);
      a2 <- arg subst(sub)) 
      yield App(f2, a2)*/
  }
  
  case class Lam(abs: \\[Term]) extends Term {
    object injectNominal extends IFunctor[Term, Nominal] {
      def inject[I[+_]](f: InjFun[I])(implicit idi: Idiom[I]) = idi.c(Lam) >> f(abs)
    }
    object injectSubstable extends IFunctor[Term, SubstableTo] {
      def inject[I[+_]](f: InjFun[I])(implicit idi: Idiom[I]) = idi.c(Lam) >> f(abs)
    }      
    
/*  def swap(a: Name, b: Name) = Lam(abs swap(a, b))
    def fresh(a: Name) = abs fresh(a)
    def supp = abs supp
    
    def subst(sub: Name => Option[Term]): AM[Term] = for(
        abs2 <- abs subst(sub))
        yield Lam( abs2 )*/
  }   
}


object Test extends AbsM with BindingSyntax with Binding with Substitution with Lambda with Application {
  println((for(
      x <- gensym("x");
      y <- gensym("y");
      z <- gensym("z");
      subXtoZ <- Lam(y\\Var(x)) subst (t => if(t == x) Some(Var(z)) else None);
      subNop <- Lam(x\\Var(x)) subst (t => if(t == x) Some(Var(z)) else None)) 
    yield (Lam(x\\Var(y)) == Lam (z\\Var(y)),
           Lam(x\\Var(y)) == Lam (y\\Var(x)),
           Lam(x\\Var(x)) == Lam (y\\Var(y)), subXtoZ, subNop
           )).run) // prints "(true,false,true,Lam(y$0\\Var(z$2)),Lam(x$0\\Var(x$0)))"
}*/